\begin{tabbing}
$\forall$\=$E$, $X_{1}$, $X_{2}$:Type, ${\it pred?}$:($E$$\rightarrow$(?$E$)), ${\it info}$:($E$$\rightarrow$((:Id $\times$ $X_{1}$) + (:(:IdLnk $\times$ $E$) $\times$ $X_{2}$))), $r_{1}$, $r_{2}$,\+
\\[0ex]$x$:$E$.
\-\\[0ex]SWellFounded(($\neg$($\uparrow$first($y$))) c$\wedge$ ($x$ = pred($y$)))
\\[0ex]$\Rightarrow$ $r_{2}$ before $r_{1}$ $\in$ eventlist(${\it pred?}$;$x$)
\\[0ex]$\Rightarrow$ $r_{2}$ $<$ $r_{1}$
\end{tabbing}